x:chain_config(). (ccpred?(x))  (ccpred-id(x)  Id) 

latex

Definitions	s = t, t  T, False, Id, , x:AB(x), P  Q, chain config ind ccsucc compseq tag def, b, ccpred?(x), ccpred-id(x), True, chain config ind ccpred compseq tag def, chain config ind cctail compseq tag def, #$n, , Type, , chain config ind cchead compseq tag def, x:A  B(x), left + right, Unit, chain_config(), x:A. B(x)
Lemmas	Id wf, member wf, assert wf, chain config wf, true wf, false wf